﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using System.IO;
using System.Diagnostics;
using System.Collections.ObjectModel;
using OpSatPlan.PlanningGraph;

namespace OpSatPlan.Encoder
{
    public class CnfEncoder
    {
        private RelaxedPlanningGraph mGraph;
        private StreamWriter mWriter;
        private int mClauses;
        private CnfVariables mVariables;
        private Input mInput;

        public CnfEncoder(RelaxedPlanningGraph graph, Input input)
        {
            this.mGraph = graph;
            this.mInput = input;
            this.mVariables = new CnfVariables();
        }

        public int NumberOfClauses
        {
            get
            {
                return this.mClauses;
            }
        }

        public int NumberOfVariables
        {
            get
            {
                return this.mVariables.NumberOfVariables;
            }
        }

        public void Reset()
        {
            this.mClauses = 0;
            if (File.Exists(this.CnfFileName))
                File.Delete(this.CnfFileName);
            this.mVariables.Reset();
            this.mWriter = new StreamWriter(this.CnfFileName);
        }

        public void Encode()
        {
            
            StateEncoder stateEncoder;
            OperatorEncoder opEncoder;
            OperatorDrillDownEncoder drillEncoder;
            MutexEncoder mutexEncoder;
            EfaEncoder efaEncoder;
            Level level;

            stateEncoder = new StateEncoder(this);
            opEncoder = new OperatorEncoder(this);
            drillEncoder = new OperatorDrillDownEncoder(this);
            mutexEncoder = new MutexEncoder(this);
            efaEncoder = new EfaEncoder(this);

            // populate variables
            List<AtomicFormula> allVars;

            allVars = (from vaf in this.mGraph.GetLastLevel().PositiveEndLiterals
                      select vaf.AtomicFormula).ToList();



            allVars.AddRange(from vaf in this.mGraph.GetLastLevel().NegativeEndLiterals
                             where !allVars.Contains(vaf.AtomicFormula)
                             select vaf.AtomicFormula);

            for (int i = 0; i < this.mGraph.TimeSteps; i++)
            {
                level = this.mGraph.GetLastLevel();
                foreach (AtomicFormula af in allVars)
                    this.mVariables.GetVariable(af, i);
                foreach (Operator op in level.Operators)
                    this.mVariables.GetVariable(op, i);
            }

            // write out a string of 50 spaces as place holder.
            this.mWriter.WriteLine(new string(' ', 50));

            // encode initial state
            stateEncoder.Encode(this.mGraph.Problem.InitialState.ToList(), 0);

            var negs = from af in allVars
                       where this.mGraph.Problem.InitialState.All(vaf => vaf.AtomicFormula != af)
                       select new ValuedAtomicFormula(af, false);

            stateEncoder.Encode(negs.ToList(), 0);

            level = this.mGraph.GetLastLevel();
			
            foreach (Operator op in level.Operators)
                opEncoder.Encode(op);

            drillEncoder.Encode(level.Operators);

            mutexEncoder.Encode(level.Operators);

            efaEncoder.Encode(level.Operators, allVars);

            // encode goal state
            stateEncoder.Encode(this.mGraph.Problem.GoalState.ToList(), this.mGraph.TimeSteps);

            this.mWriter.Close();

            // add the header to the file
            this.AddCnfHeader();
        }

        internal void WriteClause(string clause)
        {
            this.mWriter.WriteLine(clause);
            this.mClauses++;
        }

        internal void WriteClauses(ClauseTemplate clause)
        {
            for (int i = 0; i < this.mGraph.TimeSteps; i++)
            {
                this.WriteClause(clause.GenerateClause(i));
            }
        }
        private void AddCnfHeader()
        {
            // overwrite place holder with cnf problem header
            BinaryWriter bw = new BinaryWriter(File.Open(this.CnfFileName, FileMode.Open));

            // seek beginning of the file.
            bw.Seek(0, SeekOrigin.Begin);

            // write out header with number of variables and clauses.
            bw.Write(Encoding.ASCII.GetBytes("p cnf " + (this.NumberOfVariables) + " " + this.mClauses));
            bw.Close();
        }

        public string CnfFileName
        {
            get
            {
                return System.IO.Path.GetFileNameWithoutExtension(this.mInput.ProblemFileName) + 
                        "_cnf_" + System.Diagnostics.Process.GetCurrentProcess().Id.ToString() + ".txt";
            }
        }

        public Planner.Plan GetPlan(bool?[] model)
        {
            Planner.Plan plan;
            ReadOnlyCollection<int> cnfActionVars;
            int timeStep;
            List<AtomicFormula> preAf;
            List<AtomicFormula> delAf;
            List<AtomicFormula> addAf;
            Operator op;
          
            plan = new Planner.Plan(this.mGraph.TimeSteps);
            cnfActionVars = this.mVariables.ActionCnfValues;

            var res = from aVar in cnfActionVars
                      where model[aVar - 1] == true
                      select aVar;

            foreach (int aVar in res)
            {
                timeStep = this.mVariables.GetTimeStep(aVar);
                op = this.mVariables.GetOperator(aVar);

                preAf = this.GetPredicates(timeStep, model, true);
                delAf = this.GetPredicates(timeStep + 1, model, false);
                addAf = this.GetPredicates(timeStep + 1, model, true);
                

                var actRes = from act in op.Actions
                           where act.Preconditions.All(p => preAf.Contains(p)) &&
                            act.AddEffects.All(p => addAf.Contains(p)) &&
                            act.DeleteEffects.All(p => delAf.Contains(p))
                           select act;
                foreach (Action a in actRes)
                    plan.Add(a, timeStep);

            }
            return plan;
        }

        private List<AtomicFormula> GetPredicates(int timeStep, bool?[] model, bool value)
        {
            List<AtomicFormula> afs = new List<AtomicFormula>();
            ReadOnlyCollection<int> vars = this.mVariables.GetPredicateCnfValues(timeStep);
            var res = from pv in vars where model[pv - 1] == value select pv;
            foreach (int v in res)
            {
                afs.Add(this.mVariables.GetAtomicFormula(v));
            }
            return afs;
        }
        public int GetTimeStep(int var)
        {
            return this.mVariables.GetTimeStep(var);
        }
        public AtomicFormula GetAtomicFormula(int var)
        {
            return this.mVariables.GetAtomicFormula(var);
        }
        public Operator GetOperator(int var)
        {
            return this.mVariables.GetOperator(var);
        }
        public int GetVariable(ValuedAtomicFormula vaf, int level)
        {
            return this.mVariables.GetVariable(vaf, level);
        }
        public int GetVariable(AtomicFormula af, int level)
        {
            return this.mVariables.GetVariable(af, level);
        }
        public bool CheckVariable(ValuedAtomicFormula vaf, int level)
        {
            return this.mVariables.CheckVariable(vaf, level);
        }
        public bool CheckVariable(AtomicFormula af, int level)
        {
            return this.mVariables.CheckVariable(af, level);
        }
        public int GetVariable(Operator op, int level)
        {
            return this.mVariables.GetVariable(op, level);
        }

    }
}
